1. Field of the Invention
This invention relates generally to circuit equivalence checking, and more particularly to circuit equivalence checking using don't care gates.
2. Description of the Related Art
Logic verification denotes the problem of showing the equivalence between a specification of the intended behavior and a description of the implemented design. At first, simulation is used to carry out logic verification. As the scale of integrated circuits become very large, simulation method become not only very time consuming but also incompetent.
Reduced ordered binary decision diagrams (ROBDDs or BDDs) have been developed, R. E. Bryant, “Graph-based Algorithms for Boolean Function Manipulation,” IEEE Trans. Computers., vol. 35, no. 8, pp. 677-691, August 1986, and formal verification has become a practical tool for replacing the function verification part of simulation. Although the success of BDDs is due to its canonical and compact representation of Boolean function, it also suffers two main drawbacks. First, it has memory explosion problem, see R. E. Bryant, “On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication,” IEEE Trans. Computers., vol. 40, no. 2, pp. 205-213, Feb. 1991. Second, it is effective for showing two designs are functional equivalent, but it is not effective for finding differences between designs.
For designs that have differences, those techniques used by automatic test pattern generation (ATPG) are more effective, D. Brand, “Verification of Large Synthesized Designs,” Proc. 1993 IEEE Intl. Conf. on CAD, pp. 534-537, November 1993. Boolean gates have been transformed to propositional clauses, T. Larrabee, “Test Pattern Generation Using Boolean Satisfiability,” IEEE Trans. Computer-Aided Design, vol. 11, pp. 4-15, January 1992. With this transformation, satisfiability (SAT) solving techniques then can also be used to solve ATPG and formal verification problems. Recently, SAT solving techniques have much improvement such that BDD and SAT have become the two major core engines for formal verification. See for example, J. P. Marques-Silva and K. A. Sakallah, “Grasp: A Search Algorithm for Propositional Satisfiability,” IEEE Trans. Computers, vol. 48, no. 5, pp. 506-521, May 1999; H. Zhang, “SATO: An Efficient Propositional Prover,” Int'l Conference on Automated Deduction, pp. 272-275, July 1997; and M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, “Chaff: Engineering an Efficient SAT Solver,” Proc. of 39th Design Automation Conference, pp. 530-535, June 2001.
Internal don't cares may occur in a design specified by register transfer language (RTL), D. Brand, R. A. Bergamaschi, and L. Stok, “Be Careful with Don't Cares,” Porc. 1995 IEEE Intl. Conf. on CAD, pp. 83-86, November 1995, such as the following descriptions in an RTL:                1. full_case synthesis directive,        2. parallel_case synthesis directive,        3. X-assignments,        4. index out of range, or        5. user imposed satisfiability constraints.        
U.S. Pat. No. 6,026,222 (the “'222 Patent”) discloses a combinational equivalence checking method based on a partition of the circuits. BDD is used for one partition and SAT is used for the other partition. U.S. Pat. No. 6,086,626 (the “'626 Patent”) disclose a filtering based methods for combinational equivalence checking. In addition to using BDD and ATGP techniques, '626 Patent also uses random simulation and structure hashing methods to speed up the performance of equivalence checking. Both '222 Patent and '626 Patent do not consider don't cares that may occur in RTL specified designs. Their methods are thus limited to gate-to-gate equivalence checking only.
U.S. Pat. No. 5,892,687 (the “'687 Patent”) discloses a method for representing internal don't cares that are generated from RTL descriptions. In the '687 patent, the don't care gates are for logic synthesis/optimization but not for equivalence checking. It does not show how the internal don't care gates will affect the output (external) don't care function of the designs.
U.S. Pat. No. 6,056,784 (the “'784 Patent”) discloses an equivalency method that utilizes don't cares. In the '784 patent, an interval of [m, M] Boolean functions is utilized to represent an ordered pair of (f, d) Boolean functions, where f is the care set and d is the don't care set. Designs are transformed into circuits and each gate is transformed into two gates representing m and M respectively. Equivalence checking is then carried out on those transformed circuits.
In the '784 patent, the Boolean function at any point of the design has the following behavior:
Off set: m′M′,
On set: m M, and
Don't care set: m′M.
This is equivalent to 3-valued logic with the encoding of 00 representing value 0, 11 representing value 1, and 01 representing value don't care. Under 3-valued logic, the complementation of a don't care is still a don't care, that is, x′=x. On other model of don't cares where a don't care value is either value 0 or value 1, the complementation of a don't care is different from the don't care itself, that is x′!=x. Furthermore, under such a model, x′x=0 and x′+x=1. These two don't care models have similar but not the same behavior. For example, in FIG. 1(a), the output has value don't care that is under 3-valued model, and in FIG. 1(b), the output has value 0 that is under the other model. The method disclosed in the '784 Patent is limited in that after the transformation only one don't care model can be applied for its equivalence checking. When other don't care model is required, the single don't care model based equivalence checking may not yield a correct result.
There is a need for equivalence checking that can utilize more than one type of don't care model.